|
The superposition calculus is a calculus for reasoning in equational first-order logic. It has been developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of (unfailing) Knuth–Bendix completion. It can be seen as a generalization of either resolution (to equational logic) or unfailing completion (to full clausal logic). As most first-order calculi, superposition tries to show the ''unsatisfiability'' of a set of first-order clauses, i.e. it performs proofs by refutation. Superposition is refutation-complete — given unlimited resources and a ''fair'' derivation strategy, from any unsatisfiable clause set a contradiction will eventually be derived. As of 2007, most of the (state-of-the-art) theorem provers for first-order logic are based on superposition (e.g. the E equational theorem prover), although only a few implement the pure calculus. == Implementations == * E * SPASS * Vampire * Waldmeister * Ayane at (Google Code ) == References == * ''Rewrite-Based Equational Theorem Proving with Selection and Simplification'', Leo Bachmair and Harald Ganzinger, Journal of Logic and Computation 3(4), 1994. * ''Paramodulation-Based Theorem Proving'', Robert Nieuwenhuis and Alberto Rubio, Handbook of Automated Reasoning I(7), Elsevier Science and MIT Press, 2001. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「superposition calculus」の詳細全文を読む スポンサード リンク
|